$\forall$${\it es}$:ES, $a$:Atom1, $e$:E.
\\[0ex]loc($e$) $\parallel$ $a$
\\[0ex]$\Rightarrow$ ($\forall$${\it e'}$:E. (${\it e'}$ $<$ $e$) $\Rightarrow$ ${\it e'}$ sends to loc($e$) $\parallel$ $a$ )
\\[0ex]$\Rightarrow$ es\_state\_when(${\it es}$;es{-}init(${\it es}$;$e$)):es\_state(${\it es}$;loc($e$))$\parallel$$a$
\\[0ex]$\Rightarrow$ $e$ sends $\parallel$ $a$